Computational lambda-calculus and monads
モナド云々が画期的だということでよく紹介される
主張としては、プログラム同士の同値性を考える際に従来の方法では正確性に欠けるので、より正確に扱える手法として圏論のモナドを使おうぜ！というもの
1988年
新規性
従来ではプログラムの意味論といえばラムダ計算だったが、これはβ簡約などによって同じラムダ抽象でも異なる形に表現できてしまうので、ある意味情報を損なうことになる。そこで、この意味論文やに圏論を用いた新しい計算モデルを提案。 大まかな流れ
Introduction
プログラムの等価性には3つのアプローチがあった
論理的観点からのアプローチ
なので、たとえ同じ式に簡約されたとしても、それらのプログラムの等価性を正確に同じだとは言えない
例えば副作用とかは表示されない
直積型が計算とどう結びつくのか、とか
A categorical semantics of computations
ここからが本質だが未読mrsekut.icon
Extending the language
The λc-calculus
Untyped λc-models
Reduction
Conclusions and further research
圏論をプログラム意味論のフレームワークとして使用できる
計算を改善するために、
プログラム同士の同値性を正確に導く、
という手法が使える
Acknowledgements
References
面白そうな関連論文
この論文の親にあたるもの
多分この論文のリファレンスには載っていないが、この論文の話をしてる人が挙げてた
気になった英単語・英語表現
参考